max(L(x)) → x
max(N(L(0), L(y))) → y
max(N(L(s(x)), L(s(y)))) → s(max(N(L(x), L(y))))
max(N(L(x), N(y, z))) → max(N(L(x), L(max(N(y, z)))))
↳ QTRS
↳ DependencyPairsProof
max(L(x)) → x
max(N(L(0), L(y))) → y
max(N(L(s(x)), L(s(y)))) → s(max(N(L(x), L(y))))
max(N(L(x), N(y, z))) → max(N(L(x), L(max(N(y, z)))))
MAX(N(L(x), N(y, z))) → MAX(N(y, z))
MAX(N(L(x), N(y, z))) → MAX(N(L(x), L(max(N(y, z)))))
MAX(N(L(s(x)), L(s(y)))) → MAX(N(L(x), L(y)))
max(L(x)) → x
max(N(L(0), L(y))) → y
max(N(L(s(x)), L(s(y)))) → s(max(N(L(x), L(y))))
max(N(L(x), N(y, z))) → max(N(L(x), L(max(N(y, z)))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
MAX(N(L(x), N(y, z))) → MAX(N(y, z))
MAX(N(L(x), N(y, z))) → MAX(N(L(x), L(max(N(y, z)))))
MAX(N(L(s(x)), L(s(y)))) → MAX(N(L(x), L(y)))
max(L(x)) → x
max(N(L(0), L(y))) → y
max(N(L(s(x)), L(s(y)))) → s(max(N(L(x), L(y))))
max(N(L(x), N(y, z))) → max(N(L(x), L(max(N(y, z)))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
MAX(N(L(s(x)), L(s(y)))) → MAX(N(L(x), L(y)))
max(L(x)) → x
max(N(L(0), L(y))) → y
max(N(L(s(x)), L(s(y)))) → s(max(N(L(x), L(y))))
max(N(L(x), N(y, z))) → max(N(L(x), L(max(N(y, z)))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MAX(N(L(s(x)), L(s(y)))) → MAX(N(L(x), L(y)))
The value of delta used in the strict ordering is 4.
POL(N(x1, x2)) = (2)x_2
POL(L(x1)) = (4)x_1
POL(s(x1)) = 1/2 + x_1
POL(MAX(x1)) = x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
max(L(x)) → x
max(N(L(0), L(y))) → y
max(N(L(s(x)), L(s(y)))) → s(max(N(L(x), L(y))))
max(N(L(x), N(y, z))) → max(N(L(x), L(max(N(y, z)))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
MAX(N(L(x), N(y, z))) → MAX(N(y, z))
max(L(x)) → x
max(N(L(0), L(y))) → y
max(N(L(s(x)), L(s(y)))) → s(max(N(L(x), L(y))))
max(N(L(x), N(y, z))) → max(N(L(x), L(max(N(y, z)))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MAX(N(L(x), N(y, z))) → MAX(N(y, z))
The value of delta used in the strict ordering is 8.
POL(N(x1, x2)) = 2 + (4)x_1 + (2)x_2
POL(L(x1)) = 0
POL(MAX(x1)) = (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
max(L(x)) → x
max(N(L(0), L(y))) → y
max(N(L(s(x)), L(s(y)))) → s(max(N(L(x), L(y))))
max(N(L(x), N(y, z))) → max(N(L(x), L(max(N(y, z)))))